/LMAR=0/XLINE=3/USET=79␈↓ α,␈↓␈↓ ⊂F1


















␈↓ α,␈↓α␈↓ αETHE ELEPHANT LANGUAGE FOR PROVING AND MAYBE EVEN PROGRAMMING

␈↓ α,␈↓␈↓ λby John McCarthy

␈↓ α,␈↓␈↓αAbstract:␈↓␈α⊃An␈α⊃Elephant␈α⊃program␈α⊃is␈α⊃a␈α⊃collection␈α⊃of␈α⊃sentences␈α⊃of␈α⊃≡rst␈α⊃order␈α⊃logic.␈α⊃ Corresponding
␈↓ α,␈↓to␈α↔a␈α↔program␈α↔variable␈α↔␈↓↓x␈↓␈α↔in␈α↔an␈α↔Algol-type␈α↔program,␈α↔there␈α↔is␈α↔a␈α↔function␈α↔␈↓↓x(t)␈↓␈α↔of␈α↔time␈α↔in␈α↔the
␈↓ α,␈↓Elephant␈α_program.␈α_ Sentences␈α_of␈α_≡rst␈α_order␈α_logic␈α_tell␈α_how␈α_the␈α_values␈α_of␈α_variables␈α_like␈α_␈↓↓x(t)␈↓
␈↓ α,␈↓depend␈α∩on␈α∩the␈α∩values␈α∩of␈α∩the␈α∩variables␈α∩at␈α∩earlier␈α∩times.␈α∩ The␈α∩␈↓↓program␈α∩counter␈↓␈α∩is␈α∩treated␈α∩as␈α∩just
␈↓ α,␈↓another variable.

␈↓ α,␈↓␈↓ α|Representing␈α⊂program␈α⊂variables␈α⊂as␈α⊂explicit␈α⊂functions␈α⊂of␈α⊂time␈α⊂has␈α⊂been␈α⊂explicitly␈α⊂rejected␈α⊂by
␈↓ α,␈↓many␈α⊃computer␈α⊃scientists,␈α⊃but␈α⊃it␈α⊃has␈α⊃advantages␈α⊃that␈α⊃justify␈α⊃overcoming␈α⊃their␈α⊃prejudices.␈α⊃ First,
␈↓ α,␈↓properties␈α∪of␈α∪Elephant␈α∪programs␈α∪are␈α∪expressed␈α∪as␈α∪≡rst␈α∪order␈α∪sentences␈α∪in␈α∪the␈α∪language␈α∪of␈α∪the
␈↓ α,␈↓data␈α∀domain␈α∀augmented␈α∀by␈α∀the␈α∀names␈α∀of␈α∀the␈α∀functions␈α∀constituting␈α∀the␈α∀program.␈α∀ The␈α∀usual
␈↓ α,␈↓methods␈α∪for␈α∪proving␈α∪properties␈α∪of␈α∪programs␈α∪require␈α∪no␈α∪new␈α∪"logic␈α∪of␈α∪programming";␈α∪they␈α∪are
␈↓ α,␈↓just␈α∪styles␈α∪of␈α∪proof␈α∪in␈α∪≡rst␈α∪order␈α∪logic.␈α∪ Except␈α∪in␈α∪exotic␈α∪cases,␈α∪when␈α∪the␈α∪sentences␈α∪we␈α∪want␈α∪to
␈↓ α,␈↓prove␈α∨fail␈α∨in␈α∨non-standard␈α∨models␈α∨of␈α∨arithmetic,␈α∨all␈α∨properties␈α∨of␈α∨programs␈α∨are␈α∨logical
␈↓ α,␈↓consequences␈α⊗of␈α⊗the␈α⊗sentences␈α⊗expressing␈α⊗the␈α⊗Elephant␈α⊗program␈α⊗and␈α⊗the␈α⊗axioms␈α⊗of␈α⊗the␈α⊗data
␈↓ α,␈↓domain.␈α∀ We␈α∀make␈α∀comparisons␈α∀with␈α∀temporal␈α∀logic.␈α∀ Second,␈α∀equivalences␈α∀between␈α∀programs
␈↓ α,␈↓are␈α_conveniently␈α_expressed␈α_and␈α_proved.␈α_ Third,␈α_the␈α_sentence␈α_representing␈α_a␈α_combination␈α_of
␈↓ α,␈↓∨owcharts is just the conjunction of the sentences representing the ∨owcharts separately.

␈↓ α,␈↓␈↓ α|Besides␈α_representing␈α_ordinary␈α_sequential␈α_and␈α_parallel␈α_programs,␈α_Elephant␈α_can␈α_represent
␈↓ α,␈↓programs␈α⊂that␈α⊂refer␈α⊂to␈α⊂the␈α⊂past␈α⊂of␈α⊂variables␈α⊂and␈α⊂therefore␈α⊂avoid␈α⊂explicit␈α⊂mention␈α⊂of␈α⊂many␈α⊂data
␈↓ α,␈↓structures.␈α→ Since␈α→we␈α→often␈α→refer␈α_to␈α→the␈α→past␈α→in␈α→expressing␈α→processes␈α→in␈α→natural␈α→language,␈α→a
␈↓ α,␈↓computer language that doesn't allow it cannot claim to be "natural".
␈↓ α,␈↓␈↓ λ(incomplete draft␈↓ ⊂F2


␈↓ α,␈↓1. ␈↓αIntroduction␈↓

␈↓ α,␈↓␈↓ α|The␈α⊗Elephant␈α⊗algorithmic␈α⊗language␈α⊗represents␈α⊗program␈α⊗variables␈α⊗as␈α⊗functions␈α⊗of␈α⊗a␈α⊗time

␈↓ α,␈↓variable␈α→␈↓↓t␈↓.␈α→ Instead␈α→of␈α→a␈α→variable␈α→␈↓↓x␈↓␈α→as␈α→in␈α→an␈α→Algol␈α→program,␈α→an␈α→Elephant␈α→program␈α→has␈α→a

␈↓ α,␈↓function␈α∂␈↓↓x(t),␈↓␈α∂and␈α∂instead␈α∂of␈α∂an␈α∂assignment␈α∂statement␈α∂␈↓↓x := ...␈↓,␈α∂we␈α∂may␈α∂use␈α∂an␈α∂equation␈α∂␈↓↓x(t+1) = ...␈↓

␈↓ α,␈↓or sometimes ␈↓↓x(t) = ...␈↓.  This formalism has two uses.

␈↓ α,␈↓␈↓ α|First,␈α∩Elephant␈α∩provides␈α∩a␈α∩simple␈α∩way␈α∩of␈α∩expressing␈α∩sequential␈α∩programs␈α∩as␈α∩sentences␈α∩in␈α∩a

␈↓ α,␈↓≡rst␈α order␈α theory␈α which␈α can␈α then␈α be␈α used␈α to␈α prove␈α properties␈α of␈α the␈α program.␈α  This

␈↓ α,␈↓complements␈α∂the␈α∂≡rst␈α∂order␈α∂representation␈α∂of␈α∂recursive␈α∂programs␈α∂described␈α∂in␈α∂(Cartwright␈α∂1976)

␈↓ α,␈↓and␈α∂(Cartwright␈α∂and␈α∂McCarthy␈α∂1979)␈α∂in␈α∂that␈α∂an␈α∂Elephant␈α∂program␈α∂describes␈α∂what␈α∂is␈α∂to␈α∂happen

␈↓ α,␈↓at␈α∩successive␈α∩times␈α∩starting␈α∩with␈α∩the␈α∩initial␈α∩state,␈α∩while␈α∩a␈α∩recursive␈α∩description␈α∩describes␈α∩how␈α∩a

␈↓ α,␈↓desired␈α∂function␈α∂is␈α∂computed␈α∂with␈α∂the␈α∂help␈α∂its␈α∂values␈α∂for␈α∂simpler␈α∂sets␈α∂of␈α∂arguments.␈α∂ One␈α∂might

␈↓ α,␈↓say that Elephant is bottom-up while recursive programs are top-down.

␈↓ α,␈↓␈↓ α|Once␈α∪a␈α∪program␈α∪has␈α∪been␈α∪expressed␈α∪in␈α∪Elephant,␈α∪the␈α∪␈↓↓inductive␈α∪assertion␈↓␈α∪and␈α∪␈↓↓intermittent

␈↓ α,␈↓↓assertion␈↓␈α⊃methods␈α⊃are␈α⊃automatically␈α⊃available␈α⊃as␈α⊃particular␈α⊃techniques␈α⊃of␈α⊃making␈α⊃proofs␈α⊃within

␈↓ α,␈↓≡rst␈α~order␈α~logic.␈α~ They␈α~amount␈α~to␈α~using␈α~particular␈α~kinds␈α~of␈α~lemmas␈α~in␈α~proving␈α~theorems.

␈↓ α,␈↓Instances of the Hoare axioms are also just lemmas.

␈↓ α,␈↓␈↓ α|The␈α∩second␈α∩aspect␈α∩of␈α∩Elephant␈α∩(the␈α∩motivation␈α∩for␈α∩the␈α∩name)␈α∩is␈α∩the␈α∩ability␈α∩to␈α∩refer␈α∩to␈α∩the

␈↓ α,␈↓whole␈α⊃past␈α⊃of␈α⊃the␈α⊃variables␈α⊃without␈α⊃specifying␈α⊃data␈α⊃structures␈α⊃for␈α⊃remembering␈α⊃what␈α⊃has␈α⊃to␈α⊃be

␈↓ α,␈↓known␈α⊃in␈α⊃order␈α⊃to␈α⊃perform␈α⊃a␈α⊃current␈α⊃action.␈α⊃ Thus␈α⊃a␈α⊃reservation␈α⊃program␈α⊃written␈α⊃in␈α⊃Elephant

␈↓ α,␈↓can␈α↔say␈α↔that␈α↔a␈α↔passenger␈α↔has␈α↔a␈α↔reservation␈α↔if␈α↔he␈α↔has␈α↔made␈α↔one␈α↔and␈α↔not␈α↔cancelled␈α↔it.␈α↔ The

␈↓ α,␈↓program␈α⊃needn't␈α⊃specify␈α⊃any␈α⊃data␈α⊃structure␈α⊃for␈α⊃remembering␈α⊃who␈α⊃has␈α⊃reservations;␈α⊃␈↓↓an␈α⊃elephant

␈↓ α,␈↓↓never␈α∂forgets␈↓.␈α∂ Likewise,␈α∂the␈α∂rule␈α∂that␈α∂a␈α∂castling␈α∂move␈α∂is␈α∂prohibited␈α∂if␈α∂the␈α∂rook␈α∂or␈α∂king␈α∂involved

␈↓ α,␈↓has ever moved is directly expressible without inventing a variable to hold the information.

␈↓ α,␈↓␈↓ α|Such␈α∃reference␈α∃to␈α∃the␈α∃past␈α∃is␈α∃certainly␈α∃used␈α∃in␈α∃informal␈α∃English␈α∃descriptions␈α∃of␈α∃what␈α∃we

␈↓ α,␈↓want␈α∩a␈α∩computer␈α∩to␈α∩do.␈α∩ Therefore,␈α∩a␈α∩su≠ciently␈α∩high␈α∩level␈α∩programming␈α∩language␈α∩must␈α∩have
␈↓ α,␈↓␈↓ λ(incomplete draft␈↓ ⊂F3


␈↓ α,␈↓it.␈α⊃ On␈α⊃the␈α⊃other␈α⊃hand,␈α⊃the␈α⊃Elephant␈α⊃programs␈α⊃that␈α⊃I␈α⊃have␈α⊃been␈α⊃able␈α⊃to␈α⊃write␈α⊃that␈α⊃refer␈α⊃to␈α⊃the

␈↓ α,␈↓past␈α↔are␈α↔often␈α↔more␈α↔di≠cult␈α↔to␈α↔write␈α↔and␈α↔read␈α↔than␈α↔programs␈α↔with␈α↔explicit␈α↔data␈α↔structures.

␈↓ α,␈↓Perhaps␈α⊃I␈α⊃am␈α⊃simply␈α⊃inexperienced␈α⊃in␈α⊃writing␈α⊃Elephant␈α⊃program,␈α⊃but␈α⊃most␈α⊃likely␈α⊃extensions␈α⊃to

␈↓ α,␈↓the␈α∀formalism␈α∀are␈α∀also␈α∀needed.␈α∀ Of␈α∀course,␈α∀there␈α∀is␈α∀no␈α∀more␈α∀reason␈α∀to␈α∀make␈α∀a␈α∀fetish␈α∀out␈α∀not

␈↓ α,␈↓mentioning data structures than of not mentioning time.

␈↓ α,␈↓␈↓ α|The simplest way to begin is with examples.



␈↓ α,␈↓2. ␈↓αExpressing a sequential program in Elephant␈↓

␈↓ α,␈↓␈↓ α|Consider␈α∨the␈α∨following␈α∨Algol␈α∨60␈α∨program␈α∨fragment␈α∨(declarations␈α∨omitted)␈α∨for␈α∨doing

␈↓ α,␈↓multiplication by iterated addition:

␈↓ α,␈↓↓start:  i := n;␈↓ ¬|0
␈↓ α,␈↓↓␈↓ α|p := 0;␈↓ ¬|1
␈↓ α,␈↓↓loop:   ␈↓αif␈↓↓ i = 0 ␈↓αthen␈↓↓ ␈↓αgo to␈↓↓ done;␈↓ ¬|2
␈↓ α,␈↓↓␈↓ α|i := i - 1;␈↓ ¬|3
␈↓ α,␈↓↓␈↓ α|p := p + m;␈↓ ¬|4
␈↓ α,␈↓↓␈↓ α|␈↓αgo to␈↓↓ loop;␈↓ ¬|5

␈↓ α,␈↓↓done:

␈↓ α,␈↓One way of writing a corresponding Elephant program consists of the sentences

␈↓ α,␈↓↓∀t.[i(t+1) ␈↓ β2= ␈↓ β\IF pc(t) = start THEN n
␈↓ α,␈↓↓␈↓ β\ELSE IF pc(t) = start + 3 THEN i(t) - 1
␈↓ α,␈↓↓␈↓ β\ELSE IF start ≤ pc(t) ≤ start + 5 THEN i(t)
␈↓ α,␈↓↓␈↓ β\ELSE i(t+1)],

␈↓ α,␈↓↓∀t.[p(t+1) ␈↓ β2= ␈↓ β\IF pc(t) = start + 1 THEN 0
␈↓ α,␈↓↓␈↓ β\ELSE IF pc(t) = start + 4 THEN p(t) + m
␈↓ α,␈↓↓␈↓ β\ELSE IF start ≤ pc(t) ≤ start + 5 THEN p(t)
␈↓ α,␈↓↓␈↓ β\ELSE p(t+1)],

␈↓ α,␈↓↓␈↓and␈↓↓

␈↓ α,␈↓↓∀t.[pc(t+1) ␈↓ β2= ␈↓ β\IF pc(t) = start + 2 ∧ i(t) = 0 THEN done
␈↓ α,␈↓↓␈↓ β\ELSE IF pc(t) = start + 5 THEN start + 2
␈↓ α,␈↓↓␈↓ β\ELSE IF start ≤ pc(t) ≤ start + 5 THEN pc(t) + 1
␈↓ α,␈↓↓␈↓ β\ELSE pc(t+1)].

␈↓ α,␈↓␈↓ α|In␈α∩these␈α∩equations␈α∩␈↓↓i(t)␈↓␈α∩and␈α∩␈↓↓p(t)␈↓␈α∩replace␈α∩the␈α∩variables␈α∩␈↓↓i␈↓␈α∩and␈α∩␈↓↓p␈↓␈α∩of␈α∩the␈α∩Algol␈α∩program.␈α∩ The
␈↓ α,␈↓␈↓ λ(incomplete draft␈↓ ⊂F4


␈↓ α,␈↓function␈α⊂␈↓↓pc(t)␈↓␈α⊂is␈α⊂the␈α⊂program␈α⊂counter,␈α⊂and␈α⊂it␈α⊂takes␈α⊂values␈α⊂from␈α⊂␈↓↓start␈↓␈α⊂to␈α⊂␈↓↓start+5␈↓␈α⊂assuming␈α⊂that␈α⊂it

␈↓ α,␈↓takes␈α∂the␈α∂value␈α∂␈↓↓start␈↓␈α∂for␈α∂some␈α∂value␈α∂of␈α∂␈↓↓t␈↓.␈α∂ These␈α∂match␈α∂the␈α∂numbers␈α∂written␈α∂on␈α∂the␈α∂right␈α∂of␈α∂the

␈↓ α,␈↓Algol␈α⊃program.␈α⊃ Notice␈α⊃that␈α⊃the␈α⊃sentences␈α⊃say␈α⊃nothing␈α⊃about␈α⊃the␈α⊃values␈α⊃of␈α⊃any␈α⊃of␈α⊃the␈α⊃variables

␈↓ α,␈↓for␈α⊂values␈α⊂of␈α⊂␈↓↓pc(t)␈↓␈α⊂outside␈α⊂the␈α⊂range␈α⊂␈↓↓start␈↓␈α⊂to␈α⊂␈↓↓start+5␈↓.␈α⊂ This␈α⊂permits␈α⊂these␈α⊂values␈α⊂to␈α⊂be␈α⊂described

␈↓ α,␈↓by other sets of Elephant sentences.

␈↓ α,␈↓␈↓ α|It␈α∀should␈α∀be␈α∀apparent␈α∀from␈α∀the␈α∀example␈α∀that␈α∀any␈α∀program␈α∀made␈α∀up␈α∀of␈α∀assignments␈α∀and

␈↓ α,␈↓␈↓αgo to␈↓s can be systematically translated to an Elephant program.

␈↓ α,␈↓␈↓ α|Notice␈α∀also␈α∀that␈α∀the␈α∀length␈α∀of␈α∀the␈α∀Elephant␈α∀program␈α∀is␈α∀linear␈α∀in␈α∀the␈α∀length␈α∀of␈α∀the␈α∀Algol

␈↓ α,␈↓program.

␈↓ α,␈↓␈↓ α|Having␈α≤one␈α≤value␈α≤of␈α≤␈↓↓pc(t)␈↓␈α≤for␈α≤each␈α≤statement␈α≤in␈α≤the␈α≤Algol␈α≤program␈α≤is␈α≤unnecessary,

␈↓ α,␈↓although␈α↔it␈α↔makes␈α↔the␈α↔systematic␈α↔character␈α↔of␈α↔the␈α↔correspondence␈α↔more␈α↔apparent.␈α↔ If␈α↔we␈α↔let

␈↓ α,␈↓␈↓↓pc(t) = start␈↓␈α∂correspond␈α∂to␈α∂the␈α∂initialization␈α∂and␈α∂␈↓↓pc(t) = start+1␈↓␈α∂correspond␈α∂to␈α∂the␈α∂loop,␈α∂then␈α∂the

␈↓ α,␈↓equations become

␈↓ α,␈↓↓∀t.[i(t+1) ␈↓ β2= ␈↓ β\IF pc(t) = start THEN n
␈↓ α,␈↓↓␈↓ β\ELSE IF pc(t) = start+1 ∧ i(t) ≠ 0 THEN i(t) - 1
␈↓ α,␈↓↓␈↓ β\ELSE IF start ≤ pc(t) ≤ start+1 THEN i(t)
␈↓ α,␈↓↓␈↓ β\ELSE i(t+1)],

␈↓ α,␈↓↓∀t.[p(t+1) ␈↓ β2= ␈↓ β\IF pc(t) = start THEN 0
␈↓ α,␈↓↓␈↓ β\ELSE IF pc(t) = start+1 ∧ i(t) ≠ 0 THEN p(t) + m
␈↓ α,␈↓↓␈↓ β\ELSE IF start ≤ pc(t) ≤ start+1 THEN p(t)
␈↓ α,␈↓↓␈↓ β\ELSE p(t+1)],

␈↓ α,␈↓↓␈↓and␈↓↓

␈↓ α,␈↓↓∀t.[pc(t+1) ␈↓ β2= ␈↓ β\IF pc(t) = start+1 THEN (IF i(t) = 0 THEN done ELSE start+1)
␈↓ α,␈↓↓␈↓ β\ELSE IF start ≤ pc(t) ≤ start+1 THEN pc(t) + 1
␈↓ α,␈↓↓␈↓ β\ELSE pc(t+1)].

␈↓ α,␈↓␈↓ α|That these programs compute the product of ␈↓↓m␈↓ and ␈↓↓n␈↓ is speci≡ed by the sentence

␈↓ α,␈↓␈↓ α|␈↓↓∀t0.[pc(t0) = start ⊃ ∃t.[t ≥ t0 ∧ pc(t) = done ∧ p(t) = m*n]]␈↓.

␈↓ α,␈↓It␈α↔is␈α↔provable␈α↔from␈α↔any␈α↔≡rst␈α↔order␈α↔axiomatization␈α↔of␈α↔arithmetic␈α↔together␈α↔with␈α↔the␈α↔sentences

␈↓ α,␈↓constituting␈α∪the␈α∪program.␈α∪ No␈α∪special␈α∪axioms␈α∪for␈α∪programs␈α∪or␈α∪"logic␈α∪of␈α∪programs"␈α∪is␈α∪required.

␈↓ α,␈↓One need only apply mathematical induction to the predicate
␈↓ α,␈↓␈↓ λ(incomplete draft␈↓ ⊂F5


␈↓ α,␈↓␈↓ α|␈↓↓␈↓	F␈↓↓(j) ≡ ∃t.(pc(t) = start+2 ∧ p(t) = m(n - i(t)) ∧ i(t) = j ⊃ ∃t.(pc(t) = done ∧ p(t) = mn)␈↓

␈↓ α,␈↓The␈α⊃case␈α⊃␈↓↓j␈α⊃=␈α⊃0␈↓␈α⊃follows␈α⊃from␈α⊃the␈α⊃equation␈α⊃for␈α⊃␈↓↓pc(t+1),␈↓␈α⊃and␈α⊃the␈α⊃induction␈α⊃step␈α⊃also␈α⊃follows␈α⊃from

␈↓ α,␈↓the␈α∩Elephant␈α∩program.␈α∩ The␈α∩desired␈α∩result␈α∩is␈α∩the␈α∩conclusion␈α∩of␈α∩␈↓↓␈↓	F␈↓↓(n)␈↓,␈α∩and␈α∩the␈α∩premiss␈α∩of␈α∩␈↓↓␈↓	F␈↓↓(n)␈↓

␈↓ α,␈↓follows from the initial conditions.

␈↓ α,␈↓␈↓ α|Thus␈α∩an␈α∩entirely␈α∩conventional␈α∩mathematical␈α∩way␈α∩of␈α∩writing␈α∩recursion␈α∩equations␈α∩leads␈α∩to␈α∩a

␈↓ α,␈↓convenient␈α∪programming␈α∪language.␈α∪ It␈α∪is␈α∪tempting␈α∪to␈α∪call␈α∪the␈α∪language␈α∪Algol␈α∪50,␈α∪since␈α∪it␈α∪only

␈↓ α,␈↓uses ideas that were familiar in 1950.

␈↓ α,␈↓␈↓ α|The␈α∀proof␈α∀of␈α∀correctness␈α∀for␈α∀this␈α∀multiplication␈α∀program␈α∀is␈α∀misleadingly␈α∀simple,␈α∀since␈α∀we

␈↓ α,␈↓can␈α↔easily␈α↔write␈α↔explicit␈α↔formulas␈α↔for␈α↔␈↓↓i(t),␈↓␈α↔␈↓↓p(t),␈↓␈α↔and␈α↔␈↓↓pc(t)␈↓␈α↔and␈α↔prove␈α↔them␈α↔by␈α↔mathematical

␈↓ α,␈↓induction.␈α⊃ Typically␈α⊃proofs␈α⊃will␈α⊃be␈α⊃required␈α⊃in␈α⊃which␈α⊃it␈α⊃isn't␈α⊃possible␈α⊃to␈α⊃give␈α⊃explicit␈α⊃formulas

␈↓ α,␈↓for␈α∩the␈α∩variables␈α∩as␈α∩functions␈α∩of␈α∩time␈α∩or␈α∩for␈α∩the␈α∩value␈α∩of␈α∩␈↓↓t␈↓␈α∩for␈α∩which␈α∩the␈α∩program␈α∩terminates.

␈↓ α,␈↓Then␈α↔the␈α↔computational␈α↔content␈α↔of␈α↔the␈α↔proof␈α↔is␈α↔is␈α↔often␈α↔essentially␈α↔the␈α↔same␈α↔as␈α↔that␈α↔of␈α↔an

␈↓ α,␈↓␈↓↓inductive␈α∩assertions␈↓␈α∩proof␈α∩combined␈α∩with␈α∩induction␈α∩on␈α∩a␈α∩rank␈α∩function␈α∩of␈α∩the␈α∩variables␈α∩taking

␈↓ α,␈↓values in a suitable inductively ordered set.




␈↓ α,␈↓3. ␈↓αReversing a list␈↓

␈↓ α,␈↓␈↓ α|Reversing␈α∩a␈α∩list␈α∩provides␈α∩another␈α∩example␈α∩of␈α∩an␈α∩Elephant␈α∩program␈α∩that␈α∩can␈α∩be␈α∩compared

␈↓ α,␈↓with␈α∪a␈α∪recursive␈α∪conditional␈α∪expression␈α∪program␈α∩for␈α∪the␈α∪same␈α∪function.␈α∪ We␈α∪start␈α∪with␈α∪a␈α∪Lisp

␈↓ α,␈↓"program feature" program written in the style of Algol 60.

␈↓ α,␈↓↓␈↓ α|␈↓ β≤u := w;
␈↓ α,␈↓↓␈↓ α|␈↓ β≤v := ␈↓NIL␈↓↓;
␈↓ α,␈↓↓␈↓ α|␈↓ α,loop:␈↓ β≤␈↓αif␈↓↓ null u ␈↓αthen␈↓↓ ␈↓αgo to␈↓↓ done;
␈↓ α,␈↓↓␈↓ α|␈↓ β≤v := [␈↓αa␈↓↓ u] . v;
␈↓ α,␈↓↓␈↓ α|␈↓ β≤u := ␈↓αd␈↓↓ u;
␈↓ α,␈↓↓␈↓ α|␈↓ β≤␈↓αgo to␈↓↓ loop;


␈↓ α,␈↓␈↓ α|The corresponding Elephant program is

␈↓ α,␈↓↓∀t.[u(t+1) ␈↓ β2= ␈↓ β\IF pc(t) = 0 THEN w
␈↓ α,␈↓↓␈↓ β\ELSE IF pc(t) = 1 ∧ ¬null u(t) THEN ␈↓αd␈↓↓ u(t)
␈↓ α,␈↓␈↓ λ(incomplete draft␈↓ ⊂F6


␈↓ α,␈↓↓␈↓ β\ELSE u(t)],

␈↓ α,␈↓↓∀t.[v(t+1) ␈↓ β2= ␈↓ β\IF pc(t) = 0 THEN ␈↓NIL␈↓↓
␈↓ α,␈↓↓␈↓ β\ELSE IF pc(t) = 1 ∧ ¬null u(t) THEN ␈↓αa␈↓↓ u(t) . v(t)
␈↓ α,␈↓↓␈↓ β\ELSE v(t)]

␈↓ α,␈↓↓∀t.[pc(t+1) ␈↓ β2= ␈↓ β\IF pc(t) = 1 ∧ ¬null u(t) THEN 1
␈↓ α,␈↓↓␈↓ β\ELSE pc(t) + 1].

␈↓ α,␈↓␈↓ α|This can be compared with the LISP program ␈↓↓reverse␈↓ de≡ned by

␈↓ α,␈↓␈↓ α|␈↓↓reverse u ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ ␈↓NIL␈↓↓ ␈↓αelse␈↓↓ reverse ␈↓αd␈↓↓ u * <␈↓αa␈↓↓ u>␈↓.

␈↓ α,␈↓With␈α∪the␈α∪latter,␈α∪as␈α∪shown␈α∪in␈α∪(Cartwright␈α∪and␈α∪McCarthy␈α∪1979),␈α∪it␈α∪is␈α∪convenient␈α∪to␈α∪prove␈α∪such

␈↓ α,␈↓properties␈α∀as␈α∀␈↓↓reverse reverse u = u␈↓␈α∀and␈α∀␈↓↓reverse[u * v] = reverse v * reverse u␈↓.␈α∀ The␈α∀major␈α∀fact

␈↓ α,␈↓about the Elephant program is expressed by

␈↓ α,␈↓␈↓ α|␈↓↓∀t0.[pc(t0) = start ⊃ ∃t.[t ≥ t0 ∧ pc(t) = 2 ∧ v(t) = reverse w]]␈↓.

␈↓ α,␈↓It␈α∪can␈α∪be␈α∪proved␈α∪by␈α∪proving␈α∪that␈α∪␈↓↓length␈α∪u(t)␈↓␈α∪is␈α∪a␈α∪decreasing␈α∪function␈α∪of␈α∪␈↓↓t,␈↓␈α∪i.e.␈α∪for␈α∪any␈α∪␈↓↓t␈↓␈α∪such

␈↓ α,␈↓that ␈↓↓pc(t) < 2,␈↓ there is ␈↓↓t' > t␈↓ such that ␈↓↓length u(t') < length t␈↓, and also that

␈↓ α,␈↓␈↓ α|␈↓↓∀t.[reverse w = reverse u(t) * v(t)]␈↓.

␈↓ α,␈↓This␈α~is␈α~just␈α~another␈α~␈↓↓inductive␈α~assertions␈↓␈α~proof.␈α~ So␈α~far␈α~it␈α~seems␈α~that␈α~the␈α~most␈α~convenient

␈↓ α,␈↓technique␈α→for␈α→proving␈α→facts␈α→about␈α→Elephant␈α→programs␈α→is␈α→␈↓↓inductive␈α→assertions␈↓,␈α→which␈α→is␈α→less

␈↓ α,␈↓∨exible␈α≥than␈α≥the␈α≥technique␈α≥described␈α≥in␈α≥(Cartwright␈α≥and␈α≥McCarthy␈α≥1979)␈α≥that␈α≥uses␈α≥the

␈↓ α,␈↓␈↓↓functional␈α⊃equation␈↓␈α⊃and␈α⊃the␈α⊃␈↓↓minimization␈α⊃schema␈↓.␈α⊃ This␈α⊃is␈α⊃because␈α⊃␈↓↓inductive␈α⊃assertions␈↓␈α⊃provides

␈↓ α,␈↓no way of expressing algebraic relations among functions de≡ned by programs.

␈↓ α,␈↓␈↓ α|One␈α"mathematically␈α"straightforward␈α"way␈α"of␈α"de≡ning␈α"functions␈α"by␈α"programs␈α"is␈α"the

␈↓ α,␈↓following.␈α→ We␈α→rewrite␈α→the␈α→above␈α_equations␈α→to␈α→introduce␈α→␈↓↓w␈↓␈α→as␈α→an␈α→explicit␈α→argument␈α→of␈α→the

␈↓ α,␈↓functions␈α∂so␈α∂that␈α∂they␈α∂become␈α∂␈↓↓u(t,w),␈↓␈α∂␈↓↓v(t,w),␈↓␈α∂and␈α∂pc(t,w).␈α∂ We␈α∂then␈α∂de≡ne␈α∂a␈α∂relation␈α∂␈↓↓reverses(v,w)␈↓

␈↓ α,␈↓by

␈↓ α,␈↓␈↓ α|␈↓↓∀v w.(reverses(v,w) ≡ ∃t.(pc(t,w) = 2 ∧ v(t,w) = v))␈↓.

␈↓ α,␈↓When␈α∪we␈α∪have␈α∪proved␈α∪␈↓↓∀w␈α∪∃!v.reverses(v,w)␈↓,␈α∪≡rst␈α∪order␈α∪logic␈α∪entitles␈α∪us␈α∪to␈α∪replace␈α∪the␈α∪relation

␈↓ α,␈↓␈↓↓reverses␈↓ by a function.  We can then prove successively that this function satis≡es the relations
␈↓ α,␈↓␈↓ λ(incomplete draft␈↓ ⊂F7


␈↓ α,␈↓␈↓ α|␈↓↓reverse ␈↓NIL␈↓↓ = ␈↓NIL␈↓↓␈↓,

␈↓ α,␈↓␈↓ α|␈↓↓reverse [x . u] = reverse u * <x>␈↓

␈↓ α,␈↓␈↓ α|␈↓↓reverse reverse u = u␈↓,

␈↓ α,␈↓and

␈↓ α,␈↓␈↓ α|␈↓↓reverse[u * v] = reverse v * reverese u␈↓,

␈↓ α,␈↓where the notation is as in (McCarthy and Talcott 1979).




␈↓ α,␈↓4. ␈↓αAnother Elephant Formalism␈↓

␈↓ α,␈↓␈↓ α|The␈α∪Elephant␈α∪formalism␈α∪of␈α∪the␈α∪previous␈α∪sections␈α∪sorts␈α∪the␈α∪program␈α∪by␈α∪variables,␈α∪while␈α∪a

␈↓ α,␈↓sequential␈α⊃program␈α⊃sorts␈α⊃it␈α⊃according␈α⊃to␈α⊃the␈α⊃program␈α⊃counter.␈α⊃ The␈α⊃latter␈α⊃is␈α⊃more␈α⊃conventional

␈↓ α,␈↓and␈α∃often␈α∃more␈α∃convenient.␈α∃ Moreover,␈α∃if␈α∃we␈α∃want␈α∃to␈α∃represent␈α∃pieces␈α∃of␈α∃program␈α∃separately

␈↓ α,␈↓and combine them by taking conjunctions, sorting by program counter seems to work better.

␈↓ α,␈↓␈↓ α|Our pc-sorted Elephant involves three changes:

␈↓ α,␈↓␈↓ α|1.␈α⊂Instead␈α⊂of␈α⊂writing␈α⊂␈↓↓x(t),␈↓␈α⊂we␈α⊂write␈α⊂␈↓↓value(x,t).␈↓␈α⊂This␈α⊂allows␈α⊂us␈α⊂to␈α⊂quantify␈α⊂over␈α⊂variables␈α⊂and

␈↓ α,␈↓is useful for combining the ␈↓αelse␈↓ cases.

␈↓ α,␈↓␈↓ α|2.␈α∃Instead␈α∃of␈α∃starting␈α∃the␈α∃program␈α∃counter␈α∃at␈α∃0,␈α∃we␈α∃give␈α∃each␈α∃program␈α∃a␈α∃symbolic␈α∃entry

␈↓ α,␈↓location.␈α⊃ This␈α⊃is␈α⊃analogous␈α⊃to␈α⊃the␈α⊃machine␈α⊃language␈α⊃idea␈α⊃of␈α⊃a␈α⊃relocatable␈α⊃program,␈α⊃and␈α⊃it␈α⊃has

␈↓ α,␈↓the␈α⊗same␈α⊗use.␈α⊗ It␈α⊗enables␈α⊗us␈α⊗to␈α⊗combine␈α⊗programs␈α⊗by␈α⊗conjunction,␈α⊗and␈α⊗we␈α⊗can␈α⊗suppose␈α⊗that

␈↓ α,␈↓numerical␈α∃values␈α∃of␈α∃the␈α∃entry␈α∃locations␈α∃of␈α∃the␈α∃parts␈α∃of␈α∃the␈α∃program␈α∃are␈α∃speci≡ed␈α∃so␈α∃that␈α∃no

␈↓ α,␈↓distinct␈α⊂parts␈α⊂of␈α⊂the␈α⊂programs␈α⊂have␈α⊂the␈α⊂same␈α⊂values␈α⊂of␈α⊂the␈α⊂program␈α⊂counter.␈α⊂ Indeed␈α⊂specifying

␈↓ α,␈↓the␈α∂values␈α∂of␈α∂the␈α∂entry␈α∂locations␈α∂in␈α∂a␈α∂way␈α∂that␈α∂corresponds␈α∂to␈α∂overlapping␈α∂programs␈α∂will␈α∂usually

␈↓ α,␈↓lead to a contradiction in the combined sentence.

␈↓ α,␈↓␈↓ α|3.␈α≤We␈α≤have␈α≤one␈α≤equation␈α≤that␈α≤speci≡es␈α≤␈↓↓value(var,t+1)).␈↓␈α≤Its␈α≤right␈α≤side␈α≤is␈α≤a␈α≤conditional

␈↓ α,␈↓expression whose clauses correspond to the di≥erent values of the program counter.

␈↓ α,␈↓␈↓ α|With all these changes, our program ␈↓↓P1␈↓ for multiplication by addition is
␈↓ α,␈↓␈↓ λ(incomplete draft␈↓ ⊂F8


␈↓ α,␈↓↓∀var t.[value(var,t+1) =
␈↓ α,␈↓↓␈↓ β\IF value(pc,t) = entry1 ∧ var = i THEN n
␈↓ α,␈↓↓␈↓ β\ELSE IF value(pc,t) = entry1 + 1 ∧ var = p THEN 0
␈↓ α,␈↓↓␈↓ β\ELSE IF value(pc,t) = entry1 + 2 ∧ var = pc ∧ value(i,t) = 0 THEN exit1
␈↓ α,␈↓↓␈↓ β\ELSE IF value(pc,t) = entry1 + 3 ∧ var = i THEN value(i,t) - 1
␈↓ α,␈↓↓␈↓ β\ELSE IF value(pc,t) = entry1 + 4 ∧ var = p THEN value(p,t) + 1
␈↓ α,␈↓↓␈↓ β\ELSE IF value(pc,t) = entry1 + 5 ∧ var = pc THEN entry1 + 2

␈↓ α,␈↓↓␈↓ β\ELSE IF entry1 ≤ value(pc,t) ≤ entry1 + 5 ∧ var = pc THEN value(pc,t) + 1
␈↓ α,␈↓↓␈↓ β\ELSE IF entry1 ≤ value(pc,t) ≤ entry1 + 5 THEN value(var,t)
␈↓ α,␈↓↓␈↓ β\ELSE value(var,t+1)␈↓


␈↓ α,␈↓␈↓ α|Notice␈α≥that␈α≥there␈α≥is␈α≥one␈α≥clause␈α≥for␈α≥each␈α≥statement␈α≥in␈α≥the␈α≥Algol␈α≥program␈α≥and␈α≥three

␈↓ α,␈↓additional␈α⊂clauses.␈α⊂ The␈α⊂≡rst␈α⊂additional␈α⊂clause␈α⊂states␈α⊂that␈α⊂the␈α⊂program␈α⊂counter␈α⊂is␈α⊂increased␈α⊂by␈α⊂1

␈↓ α,␈↓within␈α⊃the␈α⊃program␈α⊃unless␈α⊃something␈α⊃else␈α⊃is␈α⊃previously␈α⊃stated␈α⊃about␈α⊃that␈α⊃value␈α⊃of␈α⊃the␈α⊃program

␈↓ α,␈↓counter.␈α↔ The␈α↔second␈α↔states␈α↔that␈α↔variables␈α↔whose␈α↔behavior␈α↔is␈α↔not␈α↔previously␈α↔speci≡ed␈α↔in␈α↔the

␈↓ α,␈↓program␈α∀retain␈α∀their␈α∀values␈α∀within␈α∀the␈α∀program␈α∀segment.␈α∀ The␈α∀last␈α∀clause␈α∀manages,␈α∀by␈α∀being

␈↓ α,␈↓tautologous,␈α↔to␈α↔say␈α↔nothing␈α↔about␈α↔what␈α↔happens␈α↔outside␈α↔of␈α↔the␈α↔range␈α↔␈↓↓entry1 ≤ pc ≤ entry1+5␈↓,

␈↓ α,␈↓thus␈α∃avoiding␈α∃interference␈α∃with␈α∃sentences␈α∃speci≡ying␈α∀other␈α∃programs␈α∃that␈α∃might␈α∃be␈α∃combined

␈↓ α,␈↓with ␈↓↓P1.␈↓

␈↓ α,␈↓␈↓ α|Indeed␈α∪suppose␈α∪␈↓↓P2␈↓␈α∪is␈α∪another␈α∪program␈α∪involving␈α∪some␈α∪of␈α∪the␈α∪same␈α∪same␈α∪variables␈α∪as␈α∪␈↓↓P1␈↓

␈↓ α,␈↓and␈α_possibly␈α_some␈α_others,␈α_and␈α_suppose␈α_we␈α_want␈α_to␈α_combine␈α_these␈α_programs␈α_so␈α_that␈α_␈↓↓P2␈↓␈α_is

␈↓ α,␈↓executed␈α~after␈α~␈↓↓P1.␈α~We␈↓␈α~need␈α~only␈α~take␈α~the␈α~conjunction␈α~of␈α~the␈α~sentences␈α~together␈α~with␈α~the

␈↓ α,␈↓sentence␈α∀␈↓↓entry2 = exit1␈↓.␈α∀ Should␈α∀we␈α∀want␈α∀to␈α∀do␈α∀so,␈α∀we␈α∀can␈α∀transform␈α∀the␈α∀conjunction␈α∀into␈α∀an

␈↓ α,␈↓equivalent␈α⊃sentence␈α⊃which␈α⊃has␈α⊃the␈α⊃same␈α⊃form␈α⊃as␈α⊃␈↓↓P1␈↓␈α⊃or␈α⊃␈↓↓P2,␈↓␈α⊃i.e.␈α⊃a␈α⊃clause␈α⊃for␈α⊃each␈α⊃statement␈α⊃and

␈↓ α,␈↓three clauses at the end.

␈↓ α,␈↓␈↓ α|Combination␈α∀by␈α∀conjunction␈α∀works␈α∀the␈α∀same␈α∀in␈α∀more␈α∀complicated␈α∀cases.␈α∀ A␈α∀program␈α∀can

␈↓ α,␈↓have␈α∂multiple␈α∂entries␈α∂and␈α∂exits,␈α∂any␈α∂exit␈α∂can␈α∂be␈α∂connected␈α∂to␈α∂any␈α∂entry␈α∂just␈α∂by␈α∂equating␈α∂suitable

␈↓ α,␈↓␈↓↓entry␈↓ and ␈↓↓exit␈↓ parameters.



␈↓ α,␈↓␈↓ α|5. ␈↓αDe≡ning Functions in Elephant␈↓
␈↓ α,␈↓␈↓ λ(incomplete draft␈↓ ⊂F9


␈↓ α,␈↓␈↓ α|Work␈α∀in␈α∀program␈α∀veri≡cation␈α∀has␈α∀most␈α∀often␈α∀concerned␈α∀itself␈α∀with␈α∀verifying␈α∀input-output

␈↓ α,␈↓relations␈α∪of␈α∪programs,␈α∪and␈α∪the␈α∪previous␈α∪section␈α∪shows␈α∪how␈α∪to␈α∪do␈α∪this␈α∪for␈α∪Elephant␈α∪programs.

␈↓ α,␈↓Indeed␈α↔some␈α↔authors␈α↔have␈α↔left␈α↔their␈α↔readers␈α↔with␈α↔the␈α↔impression␈α↔that␈α↔this␈α↔is␈α↔all␈α↔there␈α↔is␈α↔to

␈↓ α,␈↓program veri≡cation.

␈↓ α,␈↓␈↓ α|There␈α⊃is␈α⊃also␈α⊃proving␈α⊃equivalence␈α⊃of␈α⊃progams␈α⊃in␈α⊃various␈α⊃senses␈α⊃and␈α⊃proving␈α⊃properties␈α⊃of

␈↓ α,␈↓functions␈α~computed␈α~by␈α~programs.␈α~ In␈α~order␈α~to␈α~prove␈α~properties␈α~of␈α~functions␈α~computed␈α~by

␈↓ α,␈↓Elephant programs, we proceed as follows:

␈↓ α,␈↓␈↓ α|Given a relation ␈↓↓P(x,y),␈↓ we can partially de≡ne a function ␈↓↓f␈↓ by

␈↓ α,␈↓␈↓ α|1)␈↓ β≤ ␈↓↓∀x.(∃y.P(x,y) ⊃ P(x,f(x)))␈↓

␈↓ α,␈↓␈↓ α|provided␈α∀␈↓↓f␈↓␈α∀is␈α∀a␈α∀fresh␈α∀function␈α∀symbol.␈α∀ No␈α∀contradiction␈α∀arises␈α∀from␈α∀(1),␈α∀because␈α∀if␈α∀there

␈↓ α,␈↓isn't␈α_any␈α_␈↓↓y␈↓␈α_such␈α_that␈α_␈↓↓P(x,y),␈↓␈α_then␈α_␈↓↓f(x)␈↓␈α_is␈α_entirely␈α_unrestricted.␈α_ Therefore,␈α_nothing␈α_need␈α_be

␈↓ α,␈↓proved␈α∨to␈α∨entitle␈α∨us␈α∨to␈α∨write␈α∨(1).␈α∨ However,␈α∨if␈α∨␈↓↓∀x∃!y.P(x,y)␈↓␈α∨holds,␈α∨then␈α∨␈↓↓f␈↓␈α∨is␈α∨completely

␈↓ α,␈↓determined, and (1) can be used to prove its properties.

␈↓ α,␈↓␈↓ α|We can use this idea in the Elephant context to write

␈↓ α,␈↓␈↓ α|2)␈↓ β≤␈α⊂␈↓↓∀x.(∃t.(pc(t,x)␈α⊂=␈α⊂done␈α⊂∧␈α⊂∀t'(t'␈α⊂<␈α⊂t␈α⊂⊃␈α⊂pc(t')␈α⊂≠␈α⊂done))␈α⊂⊃␈α⊂pc(␈↓	t␈↓↓(x),x)␈α⊂=␈α⊂done␈α⊂∧␈α⊂∀t'.(t'␈α⊂<␈α⊂␈↓	t␈↓↓(x)␈α⊂⊃

␈↓ α,␈↓↓pc(t') ≠ done))␈↓

␈↓ α,␈↓␈↓ α|thus␈α⊂partially␈α⊂de≡ning␈α⊂a␈α⊂function␈α⊂␈↓	t␈↓,␈α⊂which␈α⊂gives␈α⊂the␈α⊂time␈α⊂at␈α⊂which␈α⊂the␈α⊂program␈α⊂terminates

␈↓ α,␈↓as␈α⊃a␈α⊃function␈α⊃of␈α⊃the␈α⊃input␈α⊃parameter␈α⊃␈↓↓x.␈↓␈α⊃If␈α⊃we␈α⊃want␈α⊃␈↓↓f(x)␈α⊃to␈↓␈α⊃be␈α⊃the␈α⊃value␈α⊃of␈α⊃the␈α⊃variable␈α⊃␈↓↓y␈↓␈α⊃when

␈↓ α,␈↓the programs gets to ␈↓↓done,␈↓ we then write

␈↓ α,␈↓␈↓ α|3)␈↓ β≤ ␈↓↓∀x.(f(x) = y(␈↓	t␈↓↓(x),x))␈↓.

␈↓ α,␈↓␈↓ α|We␈α⊂can␈α⊂then␈α⊂use␈α⊂(2)␈α⊂and␈α⊂(3)␈α⊂to␈α⊂prove␈α⊂any␈α⊂desired␈α⊂properties␈α⊂of␈α⊂␈↓↓f.␈↓␈α⊂Some␈α⊂of␈α⊂these␈α⊂properties,

␈↓ α,␈↓including␈α≥algebraic␈α≥relations␈α≥like␈α≥associativity␈α≥are␈α≥not␈α≥directly␈α≥expressible␈α≥as␈α≥input-output

␈↓ α,␈↓relations of the program.



␈↓ α,␈↓6. ␈↓αEquivalence of Elephant programs␈↓
␈↓ α,␈↓␈↓ λ(incomplete draft␈↓ ⊂010


␈↓ α,␈↓␈↓ α|De≡nitions␈α9of␈α9the␈α9equivalence␈α9of␈α9Elephant␈α9programs,␈α9equivalence-preserving

␈↓ α,␈↓transformations␈α⊗of␈α⊗programs,␈α⊗and␈α⊗techniques␈α⊗for␈α⊗proving␈α⊗equivalence␈α⊗can␈α⊗be␈α⊗expected␈α⊗to␈α⊗be

␈↓ α,␈↓important␈α≡in␈α≡applications.␈α≡ Indeed␈α≡one␈α≡approach␈α≡to␈α≡compiling␈α≡is␈α≡to␈α≡transform␈α≡a␈α≡general

␈↓ α,␈↓Elephant program into an immediate program using equivalence-preserving transformations.

␈↓ α,␈↓␈↓ α|Equivalence␈α_relations␈α_should␈α_be␈α_de≡ned␈α_that␈α_will␈α_facilitate␈α_such␈α_processes.␈α_ An␈α_obvious

␈↓ α,␈↓form␈α⊂of␈α⊂equivalence␈α⊂is␈α⊂to␈α⊂require␈α⊂that␈α⊂each␈α⊂variable␈α⊂in␈α⊂the␈α⊂two␈α⊂programs␈α⊂be␈α⊂represented␈α⊂by␈α⊂the

␈↓ α,␈↓same␈α∩function␈α∩of␈α∩time␈α∩for␈α∩all␈α∩values␈α⊃of␈α∩the␈α∩parameters.␈α∩ This␈α∩is␈α∩too␈α∩strict␈α∩an␈α∩equivalence␈α∩to␈α∩be

␈↓ α,␈↓interesting␈α∩on␈α∩two␈α∩grounds.␈α∩ First,␈α∩the␈α∩two␈α∩forms␈α∩of␈α∩the␈α∩multiplication␈α∩by␈α∩addition␈α∩program␈α∩in

␈↓ α,␈↓section␈α∩2␈α∩would␈α∩not␈α∩be␈α∩equivalent,␈α∩because␈α∩one␈α∩of␈α∩them␈α∩goes␈α∩around␈α∩the␈α∩loop␈α∩in␈α∩one␈α∩time␈α∩step

␈↓ α,␈↓while␈α∃the␈α∃other␈α∃takes␈α∃four␈α∃steps.␈α∃ Second,␈α∃transforming␈α∃a␈α∃program␈α∃to␈α∃an␈α∃immediate␈α∃program

␈↓ α,␈↓may␈α⊗involve␈α⊗the␈α⊗introduction␈α⊗of␈α⊗new␈α⊗variables,␈α⊗arrays␈α⊗and␈α⊗other␈α⊗data␈α⊗structures␈α⊗in␈α⊗order␈α⊗to

␈↓ α,␈↓eliminate the direct references to the past.

␈↓ α,␈↓␈↓ α|In␈α~fact␈α~many␈α~kinds␈α~of␈α~equivalence␈α~are␈α~useful.␈α~ We␈α~begin␈α~with␈α~a␈α~class␈α~of␈α~equivalence

␈↓ α,␈↓relations␈α∀based␈α∀on␈α∀a␈α∀notion␈α∀of␈α∀an␈α∀equivalence␈α∀between␈α∀states␈α∀of␈α∀two␈α∀programs.␈α∀ However,␈α∀we

␈↓ α,␈↓don't␈α∩want␈α∩to␈α∩assume␈α∩that␈α∩every␈α∩state␈α∩of␈α∩each␈α∩program␈α∩has␈α∩a␈α∩corresponding␈α∩state␈α∩in␈α∩the␈α∩other;

␈↓ α,␈↓only␈α→certain␈α→states␈α→will␈α→correspond.␈α→ We␈α→certainly␈α→want␈α→the␈α→beginning␈α→and␈α→ending␈α→states␈α→to

␈↓ α,␈↓correspond,␈α⊗and␈α⊗we␈α⊗also␈α⊗want␈α⊗to␈α⊗be␈α⊗sure␈α⊗that␈α⊗any␈α⊗state␈α⊗of␈α⊗one␈α⊗program␈α⊗that␈α⊗corresponds␈α⊗to

␈↓ α,␈↓another␈α∩will␈α∩eventually␈α∩be␈α∩followed␈α∩by␈α∩a␈α∩state␈α∩that␈α∩should␈α∩also␈α∩correspond.␈α∩ Here␈α∩is␈α∩how␈α∩these

␈↓ α,␈↓ideas can be formalized.

␈↓ α,␈↓␈↓ α|Let␈α∂one␈α∂Elephant␈α∂program␈α∂␈↓↓P␈↓␈α∂have␈α∂functions␈α∂␈↓↓u␈↓#v1␈↓#(t), ... ,u␈↓#vm␈↓#(t)␈↓␈α∂and␈α∂a␈α∂second␈α∂␈↓↓P'␈↓␈α∂have␈α∂functions

␈↓ α,␈↓␈↓↓u␈↓#v1␈↓#'(t) ... u␈↓#vn␈↓#'(t).␈↓␈α⊃To␈α⊃avoid␈α⊃prolixity,␈α⊃we␈α⊃summarize␈α⊃these␈α⊃functions␈α⊃as␈α⊃vectors␈α⊃␈↓↓␈↓αu␈↓↓(t)␈↓␈α⊃and␈α⊃␈↓↓␈↓αu␈↓↓'(t)␈↓.␈α⊃ Let

␈↓ α,␈↓␈↓↓EV(␈↓αu␈↓↓,␈↓αu␈↓↓')␈↓␈α∂be␈α∂a␈α∂relation.␈α∂ Let␈α∂␈↓↓P␈↓␈α∂depend␈α∂on␈α∂parameters␈α∂␈↓↓x␈↓#v1␈↓#, ... x␈↓#vp␈↓#␈↓␈α∂and␈α∂␈↓↓P'␈↓␈α∂have␈α∂parameters␈α∂␈↓↓x␈↓#v1␈↓#' ... x␈↓#vq␈↓#'␈↓,

␈↓ α,␈↓similarly␈α∂summarized␈α∂into␈α∂vectors␈α∂␈↓↓␈↓αx␈↓↓␈↓␈α∂and␈α∂␈↓↓␈↓αx␈↓↓'␈↓.␈α∂ (The␈α∂parameters␈α∂of␈α∂the␈α∂program␈α∂for␈α∂multiplication

␈↓ α,␈↓by␈α⊂addition␈α⊂were␈α⊂␈↓↓m␈↓␈α⊂and␈α⊂␈↓↓n).␈↓␈α⊂Let␈α⊂␈↓↓EP(␈↓αx␈↓↓,␈↓αx␈↓↓')␈↓␈α⊂be␈α⊂a␈α⊂relation␈α⊂between␈α⊂the␈α⊂parameter␈α⊂vectors.␈α⊂ Also␈α⊂let

␈↓ α,␈↓␈↓↓Q(␈↓αu␈↓↓)␈↓␈α∃and␈α∃␈↓↓Q'(␈↓αu␈↓↓')␈↓␈α∃be␈α∃predicates␈α∃that␈α∃say␈α∃what␈α∃states␈α∃of␈α∃the␈α∃two␈α∃programs␈α∃are␈α∃to␈α∃be␈α∃compared.

␈↓ α,␈↓Now suppose we can prove that
␈↓ α,␈↓␈↓ λ(incomplete draft␈↓ ⊂011


␈↓ α,␈↓␈↓ α|␈↓↓P ∧ P' ∧ EP(␈↓αx␈↓↓,␈↓αx␈↓↓') ⊃ EV(␈↓αu␈↓↓(0),␈↓αu␈↓↓'(0)) ∧ Q(␈↓αu␈↓↓(0)) ∧ Q'(␈↓αu␈↓↓'(0))␈↓,

␈↓ α,␈↓i.e. that the initial states of the programs are comparable and correspond, and

␈↓ α,␈↓␈↓ α|␈↓↓P ∧ P' ⊃ ∀t1 t2 t1'.[EV(␈↓αu␈↓↓(t1),␈↓αu␈↓↓'(t1')) ∧ t2 >t1 ∧ Q(␈↓αu␈↓↓(t2)) ⊃ ∃t2'.EV(␈↓αu␈↓↓(t2),␈↓αu␈↓↓'(t2'))]␈↓,

␈↓ α,␈↓i.e.␈α∃that␈α∃any␈α∃comparable␈α∃state␈α∃of␈α∃␈↓↓P␈↓␈α∃that␈α∃corresponds␈α∃to␈α∃a␈α∃state␈α∃of␈α∃␈↓↓P'␈α∃is␈↓␈α∃followed␈α∃by␈α∃another

␈↓ α,␈↓comparable state that corresponds to a state of ␈↓↓P',␈↓

␈↓ α,␈↓and going the other way

␈↓ α,␈↓␈↓ α|␈↓↓P ∧ P' ⊃ ∀t1 t1' t2'.[EV(␈↓αu␈↓↓(t1),␈↓αu␈↓↓'(t1')) ∧ t2' >t1' ∧ Q'(␈↓αu␈↓↓'(t2')) ⊃ ∃t2.EV(␈↓αu␈↓↓(t2),␈↓αu␈↓↓'(t2'))]␈↓.

␈↓ α,␈↓We␈α∂should␈α∂then␈α∂call␈α∂the␈α∂programs␈α∂␈↓↓P␈↓␈α∂and␈α∂␈↓↓P'␈↓␈α∂equivalent␈α∂with␈α∂respect␈α∂to␈α∂the␈α∂the␈α∂conditions␈α∂␈↓↓Q␈↓␈α∂and

␈↓ α,␈↓␈↓↓Q'␈↓␈α≥and␈α≥the␈α≥relations␈α≥␈↓↓EP␈↓␈α≥and␈α≥␈↓↓EV.␈↓␈α≥Note␈α≥that␈α≥we␈α≥have␈α≥used␈α≥the␈α≥programs␈α≥themselves␈α≥as

␈↓ α,␈↓hypotheses since we can regard a program as the conjunction of its constituent sentences.

␈↓ α,␈↓␈↓ α|The two versions of multiplication by addition are equivalent with respect to the predicates

␈↓ α,␈↓␈↓ α|␈↓↓EP(m,n,m',n') ≡ m=m' ∧ n=n'␈↓,

␈↓ α,␈↓␈↓ α|␈↓↓Q(i,p,pc) ≡ pc = 2 ∨ pc = done␈↓,

␈↓ α,␈↓␈↓ α|␈↓↓Q'(i',p',pc') ≡ pc' = 1 ∨ pc' = done␈↓,

␈↓ α,␈↓and

␈↓ α,␈↓␈↓ α|␈↓↓EV(i,p,pc,i',p',pc') ≡ (pc=0 ∧ pc'=0) ∨ [i=i' ∧ p=p' ∧ (pc=2 ∧ pc'=1 ∨ pc=6 ∧ pc'=2)]␈↓

␈↓ α,␈↓They␈α∩should␈α∩be␈α∩su≠cient␈α∩to␈α∩prove␈α∩that␈α∩one␈α∩program␈α∩is␈α∩correct␈α∩(according␈α∩to␈α∩the␈α∩de≡nitions␈α∩of

␈↓ α,␈↓section 2) if and only if the other is.

␈↓ α,␈↓7. ␈↓αNon Immediate Elephant Programs␈↓

␈↓ α,␈↓␈↓ α|When␈α⊃we␈α⊃translate␈α⊃an␈α⊃Algol␈α⊃program␈α⊃into␈α⊃Elephant,␈α⊃we␈α⊃get␈α⊃equations␈α⊃in␈α⊃which␈α⊃the␈α⊃␈↓↓x(t+1)␈↓s

␈↓ α,␈↓depend␈α→only␈α→on␈α→the␈α→␈↓↓x(t)␈↓s.␈α→ We␈α→will␈α→call␈α→such␈α→a␈α→program␈α→an␈α→␈↓↓immediate␈↓␈α→Elephant␈α→program.

␈↓ α,␈↓However,␈α⊗the␈α⊗recursion␈α⊗equations␈α⊗will␈α⊗still␈α⊗have␈α⊗guaranteed␈α⊗solutions␈α⊗if␈α⊗the␈α⊗␈↓↓x(t)␈↓s␈α⊗depend␈α⊗on

␈↓ α,␈↓arbitrary␈α_earlier␈α_values␈α_of␈α_␈↓↓t.␈↓␈α_This␈α_leads␈α_to␈α_a␈α_"high␈α_level"␈α_programming␈α_language␈α_with␈α_the

␈↓ α,␈↓following features:

␈↓ α,␈↓␈↓ α|1.␈α∀The␈α∀program␈α∀refers␈α∀to␈α∀the␈α∀past␈α∀through␈α∀earlier␈α∀values␈α∀of␈α∀␈↓↓t,␈↓␈α∀just␈α∀as␈α∀though␈α∀everything

␈↓ α,␈↓were remembered.
␈↓ α,␈↓␈↓ λ(incomplete draft␈↓ ⊂012


␈↓ α,␈↓␈↓ α|2.␈α∪The␈α∪compiler␈α∪is␈α∪smart␈α∪and␈α∪decides␈α∪what␈α∪data␈α∪structures␈α∪are␈α∪required␈α∪in␈α∪order␈α∪to␈α∪carry

␈↓ α,␈↓out␈α∃the␈α∃computations␈α∃without␈α∃remembering␈α∃everything.␈α∃ To␈α∃the␈α∃extent␈α∃that␈α∃compilers␈α∃can␈α∃be

␈↓ α,␈↓written␈α∪that␈α∪do␈α∪this␈α∪e≥ectively,␈α∪Elephant␈α∪is␈α∪a␈α∪"higher␈α∪level"␈α∪language␈α∪in␈α∪which␈α∪the␈α∪programer

␈↓ α,␈↓speci≡es less than in Algol, etc.



␈↓ α,␈↓8. ␈↓αAn airline reservation system␈↓

␈↓ α,␈↓␈↓ α|Consider␈α≡programming␈α≡a␈α≡trivial␈α≡airline␈α≡reservation␈α≡system.␈α≡ We␈α≡want␈α≡to␈α≡say␈α≡that␈α≡␈↓↓a

␈↓ α,␈↓↓passenger␈α⊃has␈α⊃a␈α⊃reservation␈α⊃if␈α⊃he␈α⊃has␈α⊃made␈α⊃one␈α⊃that␈α⊃has␈α⊃not␈α⊃been␈α⊃cancelled␈↓.␈α⊃ We␈α⊃do␈α⊃not␈α⊃want␈α⊃to

␈↓ α,␈↓prescribe␈α∀what␈α∀data␈α∀structures␈α∀have␈α∀to␈α∀be␈α∀kept␈α∀in␈α∀order␈α∀to␈α∀be␈α∀able␈α∀to␈α∀answer␈α∀the␈α∀question␈α∀of

␈↓ α,␈↓whether someone has a reservation.

␈↓ α,␈↓␈↓ α|This␈α≤program␈α≤replies␈α≤properly␈α≤to␈α≤requests␈α≤to␈α≤make␈α≤reservations,␈α≤cancel␈α≤them,␈α≤and␈α≤to

␈↓ α,␈↓inquiries␈α∀about␈α∀whether␈α∀a␈α∀reservation␈α∀exists.␈α∀ The␈α∀program␈α∀refers␈α∀to␈α∀its␈α∀input␈α∀in␈α∀terms␈α∀of␈α∀an

␈↓ α,␈↓abstract␈α→analytic␈α→syntax␈α→the␈α→meaning␈α→of␈α→whose␈α→mnemonic␈α→predicate␈α→and␈α→function␈α→names␈α→is

␈↓ α,␈↓hopefully␈α≥obvious.␈α≥ The␈α≥only␈α≥data␈α≥structure␈α≥explicitly␈α≥mentioned␈α≥is␈α≥the␈α≥number␈α≥of␈α≥seats

␈↓ α,␈↓currently␈α≠occupied,␈α≠and␈α≠even␈α≠that␈α≠could␈α≠be␈α≠eliminated␈α≠from␈α≠the␈α≠program.␈α≠ The␈α≠Elephant

␈↓ α,␈↓compiler,␈α∩therefore,␈α∩gets␈α∩the␈α∩honor␈α∩of␈α∩determining␈α∩what␈α∩other␈α∩data␈α∩structures␈α∩are␈α∩needed.␈α∩ We

␈↓ α,␈↓use␈α∩the␈α∩convention␈α∩of␈α∩writing␈α∩␈↓↓{x}f␈↓␈α∩instead␈α∩of␈α∩␈↓↓f(x)␈↓␈α∩when␈α∩it␈α∩is␈α∩convenient␈α∩to␈α∩write␈α∩the␈α∩argument

␈↓ α,␈↓before the function name.

␈↓ α,␈↓↓␈↓ α|∀t.[output(t+1) = {input(t)}[λ in.
␈↓ α,␈↓↓␈↓ α|␈↓ β<IF ismake in THEN ␈↓ ε4[␈↓ εLIF hasrev(maker in,t) THEN "You had it"
␈↓ α,␈↓↓␈↓ α|␈↓ εLELSE IF number(t) = N THEN "No room"
␈↓ α,␈↓↓␈↓ α|␈↓ εLELSE "You have it now"]
␈↓ α,␈↓↓␈↓ α|␈↓ β<ELSE IF iscancel in THEN ␈↓ ε4[␈↓ εLIF hasrev(maker in,t) THEN "It's cancelled"
␈↓ α,␈↓↓␈↓ α|␈↓ εLELSE "You don't have it to cancel"]
␈↓ α,␈↓↓␈↓ α|␈↓ β<ELSE IF isinquiry in THEN␈↓ ε4[␈↓ εLIF hasrev(maker in,t) THEN "You have one"
␈↓ α,␈↓↓␈↓ α|␈↓ εLELSE "You don't have one"]
␈↓ α,␈↓↓␈↓ α|␈↓ β<ELSE ␈↓NIL␈↓↓]

␈↓ α,␈↓↓␈↓ α|∀t.[number(t+1) = {input(t)}[λ in.
␈↓ α,␈↓↓␈↓ α|␈↓ β<IF ismake in THEN ␈↓ ε4[␈↓ εLIF hasrev(maker in,t) ∨ number(t) = N
␈↓ α,␈↓↓␈↓ α|␈↓ εLTHEN number(t)
␈↓ α,␈↓↓␈↓ α|␈↓ εLELSE number(t) + 1]
␈↓ α,␈↓↓␈↓ α|␈↓ β<ELSE IF iscancel in THEN ␈↓ ε4[␈↓ εLIF hasrev(maker in,t) THEN number(t) - 1
␈↓ α,␈↓␈↓ λ(incomplete draft␈↓ ⊂013


␈↓ α,␈↓↓␈↓ α|␈↓ εLELSE number(t)]
␈↓ α,␈↓↓␈↓ α|␈↓ β<ELSE number(t)]

␈↓ α,␈↓where

␈↓ α,␈↓␈↓ α|␈↓↓∀t.[hasrev(passenger,t)␈α⊗≡␈α⊗∃t1.(t1␈α⊗<␈α⊗t␈α⊗∧␈α⊗ismake␈α⊗input␈α⊗t1␈α⊗∧␈α⊗passenger␈α⊗=␈α⊗maker␈α⊗input␈α⊗t1␈α⊗∧

␈↓ α,␈↓↓number(t1) < N) ∧ ¬∃t2.(t1 < t2 < t ∧ iscancel input t2 ∧ maker input t2 = passenger))]␈↓.

␈↓ α,␈↓␈↓ α|The␈α→main␈α→di≠culty␈α→in␈α→making␈α→a␈α→compiler␈α→for␈α→Elephant␈α→is␈α→illustrated␈α→by␈α→the␈α→predicate

␈↓ α,␈↓␈↓↓hasrev.␈↓␈α∩The␈α∩compiler␈α∩has␈α∩to␈α∩understand␈α∩that␈α∩it␈α∩must␈α∩remember␈α∩successful␈α∩reservations␈α∩but␈α∩can

␈↓ α,␈↓forget␈α∃unsuccessful␈α∃attempts␈α∃at␈α∃making␈α∃a␈α∃reservation␈α∃and␈α∃that␈α∃it␈α∃can␈α∃forget␈α∃reservations␈α∃that

␈↓ α,␈↓have␈α⊃been␈α⊃cancelled.␈α⊃ Perhaps␈α⊃␈↓↓hasrev␈↓␈α⊃should␈α⊃be␈α⊃written␈α⊃using␈α⊃primitives␈α⊃that␈α⊃refer␈α⊃explicitly␈α⊃to

␈↓ α,␈↓the most recent occurrence of an event, which might permit a less intelligent compiler.

␈↓ α,␈↓9. ␈↓αParallel processes for computing a sum of functions␈↓

␈↓ α,␈↓␈↓ α|The␈α∃following␈α∃Elephant␈α∃program␈α∃computes␈α∃using␈α∃␈↓↓k␈↓␈α∃processors.␈α∃ A␈α∃master␈α∃processor␈α∃with

␈↓ α,␈↓program␈α∪counter␈α∪␈↓↓pc(t)␈↓␈α∪initializes␈α∪the␈α∪variables␈α∪␈↓↓n␈↓␈α∪and␈α∪␈↓↓s␈↓␈α∪and␈α∪starts␈α∪the␈α∪␈↓↓k␈↓␈α∪slave␈α∪processes␈α∪whose

␈↓ α,␈↓program␈α↔counters␈α↔are␈α↔written␈α↔␈↓↓pc(i,t)␈↓␈α↔at␈α↔step␈α↔1.␈α↔ A␈α↔process␈α↔needs␈α↔exclusive␈α↔access␈α↔to␈α↔␈↓↓n␈↓␈α↔when

␈↓ α,␈↓reading␈α_and␈α_incrementing␈α_it,␈α_need␈α↔exclusive␈α_access␈α_to␈α_␈↓↓s␈↓␈α_when␈α_incrementing␈α_it,␈α_and␈α_we␈α_only

␈↓ α,␈↓provide␈α∪for␈α∪exclusive␈α∪access␈α∪at␈α∪these␈α∪times.␈α∪ We␈α∪presuppose␈α∪that␈α∪computing␈α∪␈↓↓f(n)␈↓␈α∪takes␈α∪␈↓↓time(n)␈↓

␈↓ α,␈↓units␈α∪of␈α∪time,␈α∪and␈α∪these␈α∪operations␈α∪are␈α∪done␈α∪in␈α∪parallel.␈α∪ ␈↓↓pc(t)␈↓␈α∪is␈α∪the␈α∪program␈α∪counter␈α∪for␈α∪the

␈↓ α,␈↓master␈α⊂process,␈α⊂and␈α⊂␈↓↓pc(i,t)␈↓␈α⊂is␈α⊂the␈α⊂program␈α⊂counter␈α⊂of␈α⊂the␈α⊂␈↓↓i␈↓th␈α⊂slave␈α⊂process.␈α⊂ The␈α⊂updating␈α⊂of␈α⊂all

␈↓ α,␈↓variables␈α≠except␈α≠the␈α≠␈↓↓pc(i,t)␈↓␈α≠works␈α≠as␈α≠in␈α≠Algolic␈α≠programs,␈α≠but␈α≠the␈α≠latter␈α≠requires␈α≠a␈α≠more

␈↓ α,␈↓elaborate␈α≥and␈α≥somewhat␈α≥implicit␈α≥description␈α≥that␈α≥may␈α≥well␈α≥challenge␈α≥the␈α≥designer␈α≥of␈α≥an

␈↓ α,␈↓Elephant compiler.

␈↓ α,␈↓↓n(t+1)␈↓ β∩= ␈↓ β<IF pc(t) = 0 THEN 1
␈↓ α,␈↓↓␈↓ β<ELSE IF pc(i,t) = 1 ∧ n(t) ≤ N THEN n(t) + 1
␈↓ α,␈↓↓␈↓ β<ELSE n(t)

␈↓ α,␈↓↓s(t+1)␈↓ β∩= ␈↓ β<IF pc(t) = 0 THEN 0
␈↓ α,␈↓↓␈↓ β<ELSE IF pc(i,t) = 5 THEN s(t) + m(i,t)
␈↓ α,␈↓↓␈↓ β<ELSE s(t)

␈↓ α,␈↓↓m(i,t+1)␈↓ β∩= ␈↓ β<IF pc(i,t) = 3 ∧ n(t) ≤ N THEN n(t)
␈↓ α,␈↓↓␈↓ β<ELSE IF pc(i,t+1) = 4 THEN f(m(i,t))
␈↓ α,␈↓␈↓ λ(incomplete draft␈↓ ⊂014


␈↓ α,␈↓↓␈↓ β<ELSE m(i,t)

␈↓ α,␈↓↓pc(t+1) ␈↓ β∩= ␈↓ β<IF pc(t) = 1 ∧ ∃i.(pc(i,t) ≠ 0) THEN 1
␈↓ α,␈↓↓␈↓ β<ELSE pc(t) + 1


␈↓ α,␈↓↓pc(i,0) = 0

␈↓ α,␈↓↓pc(i,t) = 0 ⊃ pc(i,t+1) = IF pc(t) = 0 THEN 1 ELSE 0

␈↓ α,␈↓↓pc(i,t) = 1 ⊃ ∃!j.(pc(j,t) = 1 ∧ pc(j,t+1) = 2) ∧ ∃t'.(t < t' ≤ t+k ∧ pc(i,t') = 2)

␈↓ α,␈↓↓pc(i,t) = 1 ⊃ pc(i,t+1) = 1 ∨ pc(i,t+1) = 2

␈↓ α,␈↓↓pc(i,t) = 2 ⊃ pc(i,t+1) = IF n(t) ≤ N THEN 3 ELSE 0

␈↓ α,␈↓↓pc(i,t) = 3 ∧ pc(i,t-1) ≠ 3
␈↓ α,␈↓↓␈↓ β<⊃ ∀t'.(t ≤ t' < t + time(m(i,t)) ⊃ pc(i,t') = 3) ∧ pc(t+time(m(i,t))) = 4

␈↓ α,␈↓↓pc(i,t) = 4 ⊃ ∃!j.(pc(j,t) = 4 ∧ pc(j,t+1) = 5) ∧ ∃t'.(t < t' ≤ t + k ∧ pc(i,t') = 5)

␈↓ α,␈↓↓pc(i,t) = 5 ⊃ pc(i,t+1) = 1

␈↓ α,␈↓␈↓ α|It␈α~may␈α~be␈α~questioned␈α~whether␈α~the␈α~above␈α~Elephant␈α~program␈α~should␈α~be␈α~regarded␈α~as␈α~a

␈↓ α,␈↓"program"␈α⊃that␈α⊃can␈α⊃be␈α⊃compiled␈α⊃by␈α⊃a␈α⊃suitable␈α⊃compiler␈α⊃or␈α⊃as␈α⊃something␈α⊃between␈α⊃a␈α⊃speci≡cation

␈↓ α,␈↓and␈α∩a␈α∩program.␈α∩ Perhaps␈α∩it␈α∩is␈α∩an␈α∩example␈α∩of␈α∩that␈α∩elusive␈α∩concept␈α∩called␈α∩an␈α∩algorithm.␈α∩ Notice

␈↓ α,␈↓that␈α∃it␈α∃assumes␈α∃that␈α∃synchronization␈α∃occurs␈α∀without␈α∃specifying␈α∃any␈α∃way␈α∃of␈α∃doing␈α∃it.␈α∃ Just␈α∃the

␈↓ α,␈↓thing␈α∂to␈α∂challenge␈α∂a␈α∂smart␈α∂compiler␈α∂or␈α∂automatic␈α∂programming␈α∂system.␈α∂ On␈α∂the␈α∂other␈α∂hand,␈α∂the

␈↓ α,␈↓correctness of the Elephant program is given by the statement,


␈↓ α,␈↓and␈α→this␈α→can␈α→presumably␈α→be␈α→proved␈α→from␈α→the␈α→program.␈α→ The␈α→correspondence␈α→between␈α→this

␈↓ α,␈↓Elephant␈α≠program␈α≠and␈α≠one␈α≠that␈α≠is␈α≠more␈α≠explicit␈α≠about␈α≠synchronization␈α≠might␈α≠be␈α≠proved

␈↓ α,␈↓separately.

␈↓ α,␈↓␈↓ α|There may well be better ways of describing parallel processes in Elephant.



␈↓ α,␈↓10. ␈↓αTemporal Logic Considered Unnecessary␈↓

␈↓ α,␈↓{t| P(t}

␈↓ α,␈↓x is increasing with time
␈↓ α,␈↓␈↓ λ(incomplete draft␈↓ ⊂015


␈↓ α,␈↓P is true until the ≡rst time Q is true

␈↓ α,␈↓Relations␈α∩between␈α∩values␈α∩of␈α∩the␈α∩variables␈α∩at␈α⊃di≥erent␈α∩times␈α∩can␈α∩be␈α∩expressed␈α∩in␈α∩temporal␈α∩logic

␈↓ α,␈↓but only with extra quanti≡ers.

␈↓ α,␈↓␈↓ α|The␈α∀Elephant␈α∀approach␈α∀to␈α∀representing␈α∀programs␈α∀and␈α∀proving␈α∀their␈α∀properties␈α∀is␈α∀a␈α∀close

␈↓ α,␈↓relative␈α∀of␈α∀the␈α∀modal␈α∀logic␈α∀approach␈α∀of␈α∀(Pnueli␈α∀1978)␈α∀and␈α∀(Manna␈α∀and␈α∀Pnueli␈α∀1979).␈α∀ Their

␈↓ α,␈↓formalism␈α∀also␈α∀explicitly␈α∀refers␈α∀to␈α∀the␈α∪values␈α∀of␈α∀the␈α∀program␈α∀counter␈α∀but␈α∀treats␈α∀it␈α∀in␈α∀formally

␈↓ α,␈↓di≥erent␈α∩way␈α∩from␈α∩ordinary␈α∩program␈α∩variables.␈α∩ However,␈α∩instead␈α∩of␈α∩representing␈α∩variables␈α∩as

␈↓ α,␈↓functions␈α⊂of␈α⊂time,␈α⊂they␈α⊂use␈α⊂temporal␈α⊂operators␈α⊂␈↓↓F␈↓␈α⊂(eventually),␈α⊂␈↓↓G␈↓␈α⊂(for␈α⊂all␈α⊂future␈α⊂times)␈α⊂and␈α⊂␈↓↓X␈↓␈α⊂(at

␈↓ α,␈↓the␈α∩next␈α∩time).␈α∩ (This␈α∩is␈α∩Pnueli's␈α∩notation,␈α∩the␈α∩joint␈α∩paper␈α∩uses␈α∩the␈α∩qD,␈α∩qN␈α∩common␈α∩in␈α∩modal

␈↓ α,␈↓logic␈α∪together␈α∪with␈α∪qO␈α∪for␈α∪␈↓↓X).␈α∪ ␈↓␈α∪The␈α∪modal␈α∪logic␈α∪is␈α∪justi≡ed␈α∪in␈α∪(Manna␈α∪and␈α∪Pnueli␈α∪1979)␈α∪as

␈↓ α,␈↓follows:

␈↓ α,␈↓␈↓ α|␈↓↓"In␈α∀spite␈α∀of␈α∀these␈α∀quali≡cations␈α∀there␈α∀are␈α∀some␈α∀obvious␈α∀advantages␈α∀in␈α∀the␈α∀introduction␈α∀and

␈↓ α,␈↓↓use␈α≥of␈α≥modal␈α≥formalisms.␈α≥ It␈α≥allows␈α≥an␈α≥explicit␈α≥discrimination␈α≥of␈α≥one␈α≥parameter␈α≥as␈α≥being

␈↓ α,␈↓↓appreciably␈α≠more␈α≠signi≡cant␈α≠than␈α≠all␈α≠the␈α≠others,␈α≠and␈α≠makes␈α≠dependence␈α≠on␈α≠that␈α≠parameter

␈↓ α,␈↓↓implicit.␈α∂ Nowadays,␈α∂when␈α∂increasing␈α∂attention␈α∂is␈α∂paid␈α∂to␈α∂the␈α∂clear␈α∂correspondence␈α∂between␈α∂syntax

␈↓ α,␈↓↓and␈α∂natural␈α∂reasoning␈α∂(as␈α∂is␈α∂repeatedly␈α∂stressed␈α∂by␈α∂the␈α∂discipline␈α∂of␈α∂Structured␈α∂Programming),␈α∂it

␈↓ α,␈↓↓seems␈α⊗only␈α⊗appropriate␈α⊗to␈α⊗introduce␈α⊗extra␈α⊗structure␈α⊗into␈α⊗the␈α⊗description␈α⊗of␈α⊗varying␈α⊗situations.

␈↓ α,␈↓↓Thus␈α~a␈α~clear␈α~distinction␈α~is␈α~made␈α~between␈α~variation␈α~within␈α~a␈α~state,␈α~which␈α~we␈α~express␈α~using

␈↓ α,␈↓↓predicates␈α∂and␈α∂quanti≡ers,␈α∂and␈α∂variation␈α∂from␈α∂one␈α∂state␈α∂to␈α∂another,␈α∂which␈α∂we␈α∂express␈α∂using␈α∂modal

␈↓ α,␈↓↓operators"␈↓.

␈↓ α,␈↓␈↓ α|Manna␈α≥and␈α≥Pnueli␈α≥are␈α≥right␈α≥in␈α≥asserting␈α≥that␈α≥in␈α≥programming␈α≥variation␈α≥in␈α≥time␈α≥is

␈↓ α,␈↓especially␈α∂signi≡cant.␈α∂ Unfortunately,␈α∂expressing␈α∂temporal␈α∂variation␈α∂with␈α∂modal␈α∂operators␈α∂makes

␈↓ α,␈↓time␈α∩a␈α∩second␈α∩class␈α∩citizen␈α∩and␈α∩limits␈α∩what␈α∩can␈α∩be␈α∩conveniently␈α∩said␈α∩about␈α∩it.␈α∩ Let␈α∩us␈α∩compare

␈↓ α,␈↓some Elephant assertions with the corresponding assertions in temporal logic.

␈↓ α,␈↓1. Total correctness of a program

␈↓ α,␈↓␈↓ α|␈↓↓∀t ␈↓	F␈↓↓(x(t)) ⊃ ∃t'.(t' > t ∧ pc(t') = done ∧ qP(x(t),x(t'))␈↓
␈↓ α,␈↓␈↓ λ(incomplete draft␈↓ ⊂016


␈↓ α,␈↓␈↓ α|␈↓↓␈↓	F␈↓↓(x) ∧ x = a ⊃ F [at done ∧ qP(a,x)]␈↓

␈↓ α,␈↓2. Partial correctness of a program

␈↓ α,␈↓␈↓ α|␈↓↓∀t t'.

␈↓ α,␈↓The␈α⊂following␈α⊂examples␈α⊂taken␈α⊂from␈α⊂(Manna␈α⊂and␈α⊂Pnueli␈α⊂1979)␈α⊂Kamp␈α⊂de≡ned␈α⊂two␈α⊂tenses␈α⊂by␈α⊂the

␈↓ α,␈↓equivalences:

␈↓ α,␈↓p S q ≡ (∃t){t < n ∧ q(t) ∧ (∀t')[t < t' < n) ⊃ p(t')]}

␈↓ α,␈↓p T q ≡ (∃t){n < t ∧ q(t) ∧ (∀t')[n < t' < t) ⊃ p(t')]}

␈↓ α,␈↓Here␈α∂␈↓↓p␈α∂S␈α∂q␈↓␈α∂is␈α∂read␈α∂"␈↓↓p␈↓␈α∂since␈α∂␈↓↓q␈↓␈α∂",␈α∂and␈α∂␈↓↓p␈α∂T␈α∂q␈↓␈α∂is␈α∂read␈α∂"␈↓↓p␈↓␈α∂till␈α∂␈↓↓q␈↓␈α∂".␈α∂Kamp␈α∂(1968)␈α∂proved␈α∂that␈α∂for␈α∂dense

␈↓ α,␈↓time,␈α∂in≡nite␈α∂in␈α∂both␈α∂directions,␈α∂␈↓↓S␈↓␈α∂and␈α∂␈↓↓T␈↓␈α∂are␈α∂not␈α∂de≡nable␈α∂in␈α∂terms␈α∂of␈α∂any␈α∂unary␈α∂tenses␈α∂and␈α∂that

␈↓ α,␈↓all␈α⊃"tenses"␈α⊃can␈α⊃be␈α⊃de≡ned␈α⊃in␈α⊃terms␈α⊃of␈α⊃␈↓↓S␈↓␈α⊃and␈α⊃␈↓↓T.␈↓␈α⊃While␈α⊃this␈α⊃doesn't␈α⊃show␈α⊃that␈α⊃␈↓↓S␈↓␈α⊃and␈α⊃␈↓↓T␈↓␈α⊃can't␈α⊃be

␈↓ α,␈↓de≡ned␈α⊂in␈α⊂terms␈α⊂of␈α⊂unary␈α⊂tenses␈α⊂for␈α⊂integer␈α⊂time,␈α⊂I'll␈α⊂be␈α⊂they␈α⊂can't.␈α⊂ Moreover,␈α⊂␈↓↓T␈↓␈α⊂would␈α⊂seem␈α⊂to

␈↓ α,␈↓be an entirely relevant tense for proramming.  It says that ␈↓↓p␈↓ will be true until ␈↓↓q␈↓ becomes true.



␈↓ α,␈↓11. ␈↓αRemarks␈↓

␈↓ α,␈↓1.␈α⊗Programs␈α⊗in␈α⊗Lucid␈α⊗(Ashcroft␈α⊗and␈α⊗Wadge␈α⊗1976)␈α⊗are␈α⊗also␈α⊗collections␈α⊗of␈α⊗sentences␈α⊗in␈α⊗a␈α⊗≡rst

␈↓ α,␈↓order␈α⊃language.␈α⊃ A␈α⊃Lucid␈α⊃object␈α⊃is␈α⊃a␈α⊃vector␈α⊃of␈α⊃the␈α⊃values␈α⊃of␈α⊃a␈α⊃variable␈α⊃throughout␈α⊃time.␈α⊃ This

␈↓ α,␈↓permits␈α∪some␈α∪statements␈α∪to␈α∪be␈α∪made␈α∪in␈α∪a␈α∪very␈α∪neat␈α∪way.␈α∪ However,␈α∪it␈α∪seems␈α∪to␈α∪be␈α∪less␈α∪∨exible

␈↓ α,␈↓than␈α∪the␈α∪Elephant␈α∪device␈α∪of␈α∪admitting␈α∩the␈α∪time␈α∪as␈α∪an␈α∪explicit␈α∪parameter.␈α∪ Lucid␈α∪programs␈α∪do

␈↓ α,␈↓not␈α≥admit␈α≥␈↓αgo to␈↓s,␈α≥and␈α≥there␈α≥are␈α≥other␈α≥unexpected␈α≥restrictions.␈α≥ Perhaps␈α≥some␈α≥of␈α≥Lucid's

␈↓ α,␈↓problems would be cured by including the history of the program counter as a variable.

␈↓ α,␈↓2.␈α∀The␈α∀properties␈α∀of␈α∀Elephant␈α∀programs␈α∀don't␈α∀depend␈α∀on␈α∀time␈α∀taking␈α∀integer␈α∀values.␈α∀ All␈α∀we

␈↓ α,␈↓need␈α⊂require␈α⊂is␈α⊂that␈α⊂the␈α⊂set␈α⊂of␈α⊂times␈α⊂be␈α⊂ordered␈α⊂and␈α⊂unbounded␈α⊂above.␈α⊂ Then␈α⊂the␈α⊂≡rst␈α⊂sentence

␈↓ α,␈↓of the product program would take the form

␈↓ α,␈↓␈↓↓∀t ∃t'.[t' > t ∧ i(t') ␈↓ ∧2= ␈↓ ∧\IF pc(t) = 0 THEN n
␈↓ α,␈↓↓␈↓ ∧\ELSE IF pc(t) = 3 THEN i(t) - 1
␈↓ α,␈↓↓␈↓ ∧\ELSE i(t)].
␈↓ α,␈↓␈↓ λ(incomplete draft␈↓ ⊂017


␈↓ α,␈↓3.␈α∪It␈α∪seems␈α∪to␈α∪me␈α∪that␈α∪any␈α∪language␈α∪that␈α∪purports␈α∪to␈α∪allow␈α∪the␈α∪user␈α∪to␈α∪say␈α∪what␈α∪he␈α∪wants␈α∪the

␈↓ α,␈↓computer␈α∂to␈α∂do␈α∂in␈α∂English,␈α∂should␈α∂allow␈α∂the␈α∂executive␈α∂or␈α∂general␈α∂or␈α∂other␈α∂big␈α∂shot␈α∂to␈α∂say␈α∂that␈α∂␈↓↓a

␈↓ α,␈↓↓customer␈α→has␈α→a␈α→reservation␈α→if␈α→he␈α→has␈α→made␈α→one␈α→and␈α→it␈α→hasn't␈α→been␈α→cancelled␈↓.␈α→ The␈α→big␈α→shot

␈↓ α,␈↓certainly␈α∃doesn't␈α∃want␈α∃to␈α∃concern␈α∃himself␈α∃with␈α∃what␈α∃data␈α∃structures␈α∃are␈α∃required␈α∃in␈α∃order␈α∃to

␈↓ α,␈↓ful≡ll␈α⊃his␈α⊃wishes,␈α⊃and␈α⊃Elephant␈α⊃shows␈α⊃that␈α⊃his␈α⊃wishes␈α⊃can␈α⊃be␈α⊃stated␈α⊃without␈α⊃mentioning␈α⊃such␈α⊃a

␈↓ α,␈↓data structure.

␈↓ α,␈↓4.␈α∪In␈α∪its␈α∪present␈α∪state,␈α∪Elephant␈α∪doesn't␈α∪seem␈α∪to␈α∪be␈α∪a␈α∪very␈α∪easy␈α∪language␈α∪to␈α∪use.␈α∪ I␈α∪say␈α∪"seem",

␈↓ α,␈↓because␈α→the␈α→awkward␈α→programs␈α→may␈α→be␈α→merely␈α→a␈α→consequence␈α→of␈α→inexperience.␈α→ Of␈α→course,

␈↓ α,␈↓Algolic␈α↔programs␈α↔can␈α↔easily␈α↔be␈α↔translated␈α↔into␈α↔Elephant,␈α↔but␈α↔this␈α↔doesn't␈α↔take␈α↔advantage␈α↔of

␈↓ α,␈↓Elephant's ability to refer directly to the past.

␈↓ α,␈↓5.␈α⊂Regarded␈α⊂simply␈α⊂as␈α⊂a␈α⊂way␈α⊂of␈α⊂writing␈α⊂Algolic␈α⊂programs␈α⊂as␈α⊂logical␈α⊂sentences,␈α⊂Elephant␈α⊂plays␈α⊂a

␈↓ α,␈↓role␈α∃similar␈α∃to␈α∃that␈α∃played␈α∃by␈α∃the␈α∃Cartwright␈α∃way␈α∃of␈α∃writing␈α∃Lisp␈α∃style␈α∃recursive␈α∃conditional

␈↓ α,␈↓expression␈α∪programs␈α∪as␈α∪logical␈α∪sentences.␈α∪ In␈α∪fact␈α∪it␈α∪may␈α∪be␈α∪a␈α∪kind␈α∪of␈α∪dual␈α∪to␈α∪the␈α∪Cartwright

␈↓ α,␈↓method␈α⊃just␈α⊃as␈α⊃␈↓↓inductive␈α⊃assertions␈↓␈α⊃and␈α⊃␈↓↓subgoal␈α⊃induction␈↓␈α⊃seem␈α⊃to␈α⊃be␈α⊃duals.␈α⊃ Namely,␈α⊃Elephant

␈↓ α,␈↓programs␈α∃and␈α∃inductive␈α∃assertions␈α∃work␈α∃from␈α∃an␈α∃initial␈α∃state␈α∃and␈α∃describe␈α∃its␈α∃changes,␈α∃while

␈↓ α,␈↓Lisp␈α∩style␈α∩programs␈α∩and␈α∩subgoal␈α∩induction␈α∩work␈α∩backwards␈α∩from␈α∩desired␈α∩≡nal␈α∩result.␈α∩ Thus␈α∩it

␈↓ α,␈↓may complete a pattern of methods of program formalization.

␈↓ α,␈↓6.␈α⊃Elephant␈α⊃may␈α⊃be␈α⊃expanded␈α⊃by␈α⊃relaxing␈α⊃the␈α⊃restriction␈α⊃that␈α⊃statements␈α⊃refer␈α⊃only␈α⊃to␈α⊃the␈α⊃past.

␈↓ α,␈↓Our␈α∃big␈α∃shot␈α∃may␈α∃wish␈α∃to␈α∃say,␈α∃␈↓↓"When␈α∃the␈α∃passengers␈α∃arrive␈α∃at␈α∃the␈α∃airport␈α∃for␈α∃the␈α∃∨ight,␈α∃an

␈↓ α,␈↓↓airplane␈α∃and␈α∃a␈α∃crew␈α∃will␈α∃have␈α∃been␈α∃summoned␈α∃by␈α∃the␈α∃scheduling␈α∃program␈α∃to␈α∃∨y␈α∃them␈α∃to␈α∃their

␈↓ α,␈↓↓destination"␈↓.␈α⊂ Allowing␈α⊂the␈α⊂right␈α⊂hand␈α⊂sides␈α⊂of␈α⊂Elephant␈α⊂equations␈α⊂to␈α⊂refer␈α⊂to␈α⊂the␈α⊂future␈α⊂puts␈α⊂a

␈↓ α,␈↓heavier␈α∪burden␈α∪on␈α∪the␈α∪compiler.␈α∪ In␈α∪fact,␈α∪many␈α∪futuristic␈α∪Elephant␈α∪program␈α∪are␈α∪contradictory

␈↓ α,␈↓and␈α∩hence␈α∩uncompilable.␈α∩ Thus␈α∩a␈α∩compiler␈α∩for␈α∩futuristic␈α∩Elephant␈α∩is␈α∩really␈α∩a␈α∩kind␈α∩of␈α∩problem

␈↓ α,␈↓solver.␈α∀ Nevertheless,␈α∀this␈α∀style␈α∀of␈α∀programming␈α∀may␈α∀prove␈α∀practicaly␈α∀useful␈α∀and␈α∀theoretically

␈↓ α,␈↓illuminating.
␈↓ α,␈↓␈↓ λ(incomplete draft␈↓ ⊂018


␈↓ α,␈↓8.␈α#Church␈α#(1957)␈α#represents␈α#digital␈α#circuits␈α#as␈α#recursive␈α#systems␈α#of␈α#Boolean␈α#equations

␈↓ α,␈↓determining␈α~the␈α~behavior␈α~of␈α~a␈α~collection␈α~of␈α~Boolean␈α~variables␈α~as␈α~a␈α~function␈α~of␈α~time.␈α~ He

␈↓ α,␈↓discusses␈α→the␈α→synthesis␈α→of␈α→circuits␈α→with␈α→given␈α→behavior.␈α→ Some␈α→of␈α→his␈α→results␈α→might␈α→lead␈α→to

␈↓ α,␈↓theorems␈α∂about␈α∂classes␈α∂of␈α∂Elephant␈α∂programs␈α∂over␈α∂≡nite␈α∂domains␈α∂in␈α∂cases␈α∂where␈α∂the␈α∂≡niteness␈α∂of

␈↓ α,␈↓the domain is important.



␈↓ α,␈↓12. ␈↓αReferences␈↓

␈↓ α,␈↓␈↓αAshcroft,␈α⊃E.␈α⊃A.␈α⊃and␈α⊃W.␈α⊃W.␈α⊃Wadge␈α⊃(1976)␈↓:␈α⊃Lucid␈α⊃-␈α⊃A␈α⊃Formal␈α⊃System␈α⊃for␈α⊃Writing␈α⊃and␈α⊃Proving

␈↓ α,␈↓Programs, ␈↓↓SIAM Journal of Computing␈↓, Vol. 5, No. 3, September.

␈↓ α,␈↓␈↓αBurgess, John P. (1979)␈↓: "Logic and Time", ␈↓↓Journal of Symbolic Logic␈↓, vol. 44, No. 4, Dec. 1979.

␈↓ α,␈↓␈↓αCartwright,␈α↔R.S.␈α↔(1976)␈↓:␈α↔␈↓↓A␈α↔Practical␈α↔Formal␈α↔Semantic␈α↔De≡nition␈α↔and␈α↔Veri≡cation␈α↔System␈α↔for

␈↓ α,␈↓↓Typed␈α≡Lisp␈↓,␈α≡Ph.D.␈α≡Thesis,␈α≡Computer␈α≡Science␈α≡Department,␈α≡Stanford␈α≡University,␈α≡Stanford,

␈↓ α,␈↓California.

␈↓ α,␈↓␈↓αCartwright,␈α∀Robert␈α∀and␈α∀John␈α∀McCarthy␈α∀(1979)␈↓:␈α∀"Recursive␈α∀Programs␈α∀as␈α∀Functions␈α∀in␈α∀a␈α∀First

␈↓ α,␈↓Order␈α∂Theory",␈α∂in␈α∂E.␈α∂Blum␈α∂and␈α∂S.␈α∂Takasu␈α∂(eds.),␈α∂␈↓↓Proceedings␈α∂of␈α∂the␈α∂International␈α∂Conference␈α∂on

␈↓ α,␈↓↓Mathematical Studies of Information Processing␈↓, Springer Publishers.

␈↓ α,␈↓␈↓αChurch,␈α≡Alonzo␈α≡(1957)␈↓:␈α≡"Application␈α≡of␈α≡Recursive␈α≡Arithmetic␈α≡to␈α≡the␈α≡Problem␈α≡of␈α≡Circuit

␈↓ α,␈↓Synthesis",␈α⊃in␈α⊃␈↓↓Summaries␈α⊃of␈α⊃talks␈α⊃presented␈α⊃at␈α⊃the␈α⊃Summer␈α⊃Institute␈α⊃for␈α⊃Symbolic␈α⊃Logic,␈α⊃Cornell

␈↓ α,␈↓↓University 1957␈↓., Institute for Defense Analyses.

␈↓ α,␈↓␈↓αFrancez,␈α≤Nissim␈α≤and␈α≤Amir␈α≤Pnueli␈α≤(1978)␈↓:␈α≤"A␈α≤Proof␈α≤Method␈α≤for␈α≤Cyclic␈α≤Programs",␈α≤␈↓↓Acta

␈↓ α,␈↓↓Informatica␈↓ 9, 133-157.

␈↓ α,␈↓␈↓αFrancez,␈α∀Nissim␈α∀(1976)␈↓:␈α∀␈↓↓The␈α∀Analysis␈α∀of␈α∪Cyclic␈α∀Programs␈↓,␈α∀PhD␈α∀Thesis,␈α∀Weizmann␈α∀Institute␈α∀of

␈↓ α,␈↓Science, Rehovot, Israel.

␈↓ α,␈↓␈↓αFrancez,␈α⊃Nissim␈α⊃(1978)␈↓:␈α⊃"An␈α⊃Application␈α⊃of␈α⊃a␈α⊃Method␈α⊃for␈α⊃Analysis␈α⊃of␈α⊃Cyclic␈α⊃Programs",␈α⊃␈↓↓IEEE

␈↓ α,␈↓↓Transactions on Software Engineering␈↓, vol. SE-4, No. 5, pp. 371-378, September 1978.

␈↓ α,␈↓␈↓αKamp, Hans (1968)␈↓: ␈↓↓On Tense Logic and the Theory of Order␈↓, PhD Thesis, U.C.L.A.
␈↓ α,␈↓␈↓ λ(incomplete draft␈↓ ⊂019


␈↓ α,␈↓␈↓αKroger,␈α⊃F.␈α⊃(1978)␈↓:␈α⊃"A␈α⊃Uniform␈α⊃Logical␈α⊃Basis␈α⊃for␈α⊃the␈α⊃Description,␈α⊃Speci≡cation␈α⊃and␈α⊃Veri≡cation

␈↓ α,␈↓of Programs", in E.J. Neuhold (ed.),

␈↓ α,␈↓␈↓αManna,␈α∩Zohar␈α∩and␈α∩Amir␈α∩Pnueli␈α∩(1979)␈↓:␈α∩␈↓↓The␈α⊃Modal␈α∩Logic␈α∩of␈α∩Programs␈↓,␈α∩preliminary␈α∩version␈α∩of

␈↓ α,␈↓technical␈α∃report,␈α∃Computer␈α∃Science␈α∃Department,␈α∃Stanford␈α∃University.␈α∃ ␈↓↓Formal␈α∃Descriptions␈α∃of

␈↓ α,␈↓↓Programming Concepts␈↓, North-Holland.

␈↓ α,␈↓␈↓αMcCarthy,␈α&John␈α&and␈α&Carolyn␈α&Talcott␈α&(1980)␈↓:␈α&␈↓↓LISP:␈α&Programming␈α&and␈α&Proving␈↓,␈α&(in

␈↓ α,␈↓preparation)

␈↓ α,␈↓␈↓αPnueli,␈α∂A.␈α∂(1978)␈↓:␈α∂␈↓↓The␈α∂Temporal␈α∂Semantics␈α∂of␈α∂Concurrent␈α∂Programs␈↓,␈α∂Technical␈α∂Report,␈α∂Tel-Aviv

␈↓ α,␈↓University.

␈↓ α,␈↓␈↓αPrior, A. N. (1967)␈↓: ␈↓↓Past, Present and Future␈↓, Oxford.

␈↓ α,␈↓␈↓αRescher,␈α∩Nicholas␈α∩and␈α∩Alasdair␈α∩Urquhart␈α∩(1971)␈↓:␈α∩␈↓↓Temporal␈α∩Logic␈↓,␈α∩Springer-Verlag,␈α∩New␈α∩York

␈↓ α,␈↓and Vienna.


␈↓ α,␈↓This partial draft of ELEPHA[S80,JMC] compiled at 11:04 on March 3, 1987.
/FONT#0=BASL10[300,SYS]/FONT#1=BASI10[300,SYS]=∧¬λ⊃∀∃≠≤≥≡∨ !"'()*+,-.012345679:;<=>ACDEFGHIJLMNOPQSTUVWXY[]←abcdefghijklmnopqrstuvwxyz{}}/FONT#2=BASB10[300,SYS]=≡ (),.0156789:ABCDEFGHIJKLMNOPRSTUVWYZabcdefghiklmnopqrstuvwxyzz/FONT#9=GRKB10[300,SYS]=Ftt